package ch.epfl.lara.matcheck.ast.parser;


import scala.util.parsing.input.Reader
import scala.util.parsing.combinator.{ImplicitConversions}
import scala.util.parsing.combinator.syntactical.StdTokenParsers
import scala.util.parsing.combinator.lexical.StdLexical
import scala.util.parsing.syntax.StdTokens
import scala.util.parsing.input.StreamReader

import java.io.{File,FileInputStream,InputStreamReader,StringReader}




trait MatcheckParser extends  SyntaxParser with FormulaParser { self: SyntaxParser => 
  
  
  // Keywords
  getLexical.reserved ++= List("constraints","of",
                            "object", "class", "extends", "abstract","sealed",   // class and object decl
                            "override", "def",                                   // methods decl
                            "val",                                               // fields visibility
                            "Option", //"List","Seq",                               // built-in type
                            "true","false",                                      // values
                            "new",                                               // create value
                            //"this",                                              // self reference
                            "if", "else", "match", "case","_",                   // constructs
                            "isInstanceOf",                                      // operator
                            "invariant","precondition","postcondition",
                            "constraint", "domain"
                           )


                           
  
  /** <pre>
   *    Program  ::= [ Constraints ] [Extractor Domains] { ObjectDef | ClassDef } 
   * </pre>
   */    
  def Prog: Parser[Program] = positioned(
        opt(Constraint) ~ opt(ExtractorDom) ~ rep(ObjDef | ClsDef)   
             ^^ { case constr ~ extr ~ objs_clss => 
                               val decls = split(objs_clss); 
                               Program(constr,extr,decls._1,decls._2)
                        }
      | failure("illegal start of program definition")
  )
  
  
  /**
   * Constraint ::= "/*"  "constraint"  Formula  "*/"
   */
  def Constraint: Parser[Formula] = positioned(
      "/*" ~ "constraint" ~> F <~ "*/"  
    | failure("illegal start of program definition")
  )
  
   /**
   * ExtractorDom ::= "/*"  "domain"  Domain  "*/"
   */
  def ExtractorDom: Parser[Formula] = positioned(
      "/*" ~ "domain" ~> DomainFormula <~ "*/"  
    | failure("illegal start of program definition")
  )
  
  
  /**
   * <p>
   *	Split object and class declaration.
   * </p>
   * @param objs_clss: List of mixed class and object declaration
   * @return         : A pair whose first element contains the list of object 
   *	               and the second element the list of classes.
   */
  private def split(objs_clss: List[TopDecl]): (List[ObjectDef],List[ClassDef]) = {
     def iterate(elements: List[TopDecl], acc: (List[ObjectDef],List[ClassDef])): (List[ObjectDef],List[ClassDef]) = 
       elements match {
         case Nil => acc
         case (o : ObjectDef) :: rest => iterate(rest, (acc._1 ::: List(o),acc._2))
         case (c : ClassDef) :: rest => iterate(rest, (acc._1,acc._2 ::: List(c)))
       }
     iterate(objs_clss,(Nil,Nil))
  }
  

  /** 
   * ObjectDef ::= "object" D  [ "{" [ Invariant ] { MethodDef } "}" ]
   *  
   */
  def ObjDef: Parser[TopDecl] = positioned(
        "object" ~> ident ~ opt("{" ~> opt(Invariant) ~ rep(MethDef) <~ "}")   ^^ {case name ~ inv_methods => mkObject(name,inv_methods)}
      | failure("illegal start of object definition")
  )
  
  
  /**
   * <p>
   *	Make an object out of its parsed elements.
   * </p>
   * @param name      : The parse name of the object
   * @param inv_methds: An option that contains a product with an optional 
   *			invariant and a list of method declaration 
   * @return	     : The object tree node
   */  
  private def mkObject(name: String,inv_meths: Option[~[Option[Formula],List[MethodDef]]]): ObjectDef = {
    val (inv,methods) = (inv_meths match {
      case None => (None,Nil)
      case Some(~(i,m)) => (i,m)
    })
    ObjectDef(new Name[ObjectSymbol](name),inv,methods)
  }
  
  /**
   * TypeList ::= Type { "," Type }
   */
  def TypeList: Parser[List[TypeTree]] = (
        Type ~ rep( "," ~> Type)  ^^  { case x ~ xs => x :: xs}
      | success(Nil: List[TypeTree])
  )
  
  
  /**
   * TypeTuple ::= "(" Type { "," Type } ")"
   */
  def TypeTuple: Parser[List[TypeTree]] = (
        "(" ~> TypeList <~ ")" 
      | failure("illegal start of tuple type definition")
  )
  
  
  /**
   * VarList ::= ident { "," ident }
   */
  def VarList: Parser[List[String]] = (
        ident ~ rep( "," ~> ident)  ^^  {case name ~ xs => name :: xs}
      | success(Nil: List[String])
  )
   
  /** 
   *  ClassDef ::= "class" C " [ (" ParamList ")" ]  [ "extends" D ]  [ "{" [ Invariant ] { MethodDef } "}" ]
   */
  def ClsDef: Parser[TopDecl] = positioned(
      opt("sealed") ~ opt("abstract") ~ "class" ~ ident ~ opt("(" ~> FieldList <~ ")") ~ 
        opt("extends" ~> ident) ~ opt("{" ~> opt(Invariant) ~ rep(MethDef) <~"}")      
          ^^ { case seald ~ abstr ~ "class" ~ name ~ fields ~ superc ~ inv_methds => 
                          mkClass(seald.isDefined,abstr.isDefined,name,fields,superc,inv_methds)}
      | failure("illegal start of class definition")
  )
  
  /**
   * <p>
   *	Make a class out of its parsed elements.
   * </p>
   * @param isAbs    : A boolean stating if the class is declared abstract
   * @param name     : The class' name
   * @param fields   : An optional List of parameters declaration
   * @param superc   : An optional superclass name
   * @param inv_meths: An optional product pair containing an optional class 
   *		       invariant and a list of method declaration
   * @return	     : The class tree node 
   */
  private def mkClass(isSealed: Boolean, isAbs: Boolean,name: String, fields: Option[List[FieldDef]], 
                      superc: Option[String], 
                      inv_meths: Option[~[Option[Formula],List[MethodDef]]]): ClassDef = {
     val (inv,methods) = (inv_meths match {
       case None => (None,Nil)
       case Some(~(i,m)) => (i,m)
     })
     ClassDef(isSealed,isAbs,new Name[ClassSymbol](name),fields.getOrElse(Nil),superc,inv,methods)
  }
  
  
  /**
   * Invariant ::= "/*" "invariant" Formula "*/"
   */
  def Invariant: Parser[Formula] = positioned(
      "/*" ~ "invariant" ~> F <~ "*/"    
    | failure("illegal start of class invariant definition")
  )
  
  
  /** <pre>
   *    MethodDef ::= [ "override" ] "def" ident "(" ParamList ")" ":" Type "="  [ PPC ] Expr
   *  </pre>
   */
  def MethDef: Parser[MethodDef] = positioned(
        "def" ~> ident ~ "(" ~ ParamList ~ ")"  ~ ":" ~
          Type ~ "=" ~ opt(PPC) ~ Expr ^^ { case name ~ "(" ~ params ~ ")" ~ ":" ~ tpe ~ "=" ~ ppc ~ body =>  
                                                      MethodDef(new Name[MethodSymbol](name),params,tpe,ppc,body)
                                                  }
      | failure("illegal start of method definition")
  )
  
  
  /**
   * "/*" [ "precondition" Formula ] [nl] [ "postcondition" Formula ] "*/"
   */
  def PPC: Parser[(Formula,Formula)] = (
  	"/*" ~> opt("precondition"  ~> F) 
  	     ~ opt("postcondition" ~> F) <~ 
  	"*/"  ^^ { case pre ~ post => (pre.getOrElse(Tru),post.getOrElse(Tru))}   
      | failure("illegal start of pre/post-condition definition")
  )
  
  
  /** <pre>
   *    ParamDef ::= ident ":" ident
   *  </pre>
   */
  def ParDef: Parser[ParamDef] = positioned(
        ident ~ ":" ~ Type ^^ {case name ~ ":" ~ tpe => ParamDef(new Name[VarSymbol](name),tpe)}
      | failure("illegal start of parameter definition")   
  )
  
  
  /** <pre>
   *    ParamList ::= ParamDef { "," ParamDef }
   *  </pre>
   */
  def ParamList: Parser[List[ParamDef]] = (
        ParDef ~ rep("," ~> ParDef ) ^^ { case param ~ params => param :: params } 
      | success(Nil: List[ParamDef])
  )
  
  
  /**
   * FieldDef ::= "val" ParDef
   */
  def FieldDefs: Parser[FieldDef] = positioned(
      "val"~> ident ~ ":" ~ Type ^^ { case name ~ ":" ~ tpe => FieldDef(new Name[FieldSymbol](name),tpe)} 
    | failure("illegal start of field definition")
  )
  
  
  /** <pre>
   *    ParamList ::= ParamDef { "," ParamDef }
   *  </pre>
   */
  def FieldList: Parser[List[FieldDef]] = (
        FieldDefs ~ rep("," ~> FieldDefs ) ^^ { case param ~ params => param :: params } 
      | success(Nil: List[FieldDef])
  )
  
  
  /**
   * Type ::=   ident 
   *	      | "Option" "[" ( TypeTuple | Type ) "]" 
   *	      | "List" "[" ( TypeTuple | Type ) "]"
   */
  def Type: Parser[TypeTree] = positioned(
        ident ~ opt( "[" ~> Type  <~ "]")  ^^ { case tpe ~ ptpe =>  toType2(tpe,ptpe)}
      | "Option" ~> "[" ~> ( TypeTuple | Type ) <~ "]" ^^ {case x => x match {case e: TypeTree => OptionType(List(e))
                                                                       case e: List[a]  =>  OptionType(e.asInstanceOf[List[TypeTree]])}}                                             
      | failure("illegal start of type declaration")
  )
  
  
  /** <pre>
   *    Expressions ::=   [ Expr { "," Expr } ]
   *  </pre>
   */
  def Expressions: Parser[List[Expr]] = (
      Expr ~ rep("," ~> Expr)  ^^ { case e ~ es => e :: es }
    | success(Nil: List[Expr])
  )
  
  
  /** <pre>
   *    Expr ::= OrExpr
   *  </pre>
   */
  def Expr: Parser[Expr] = positioned(
         OrExpr
      |  failure("illegal start of expression")                 
  )
    
  
  /** <pre>
   *    NegExpr ::= "!" OrExpr | OrExpr
   *  </pre>
   */
  def NegExpr: Parser[Expr] = positioned(
         "!" ~> CmpExpr                   ^^ { case expr => new !(expr)}
      |  CmpExpr
      |  failure("illegal start of expression")
  )
  
  /** <pre>
   *    OrExpr ::= AndExpr [ "||" OrExpr]
   *  </pre>
   */
  def OrExpr: Parser[Expr] = positioned(
        AndExpr ~ opt("||" ~> OrExpr) ^^ { case and ~ or => or match {
                                                                 case None => and
                                                                 case Some(x) => ||(and,x)
                                                }}
      | failure("illegal start of <or> expression")
  )
  
  /** <pre>
   *    AndExpr ::= CmpExpr [ "&&" AndExpr]
   *  </pre>
   */
  def AndExpr: Parser[Expr] = positioned(
          NegExpr ~ opt("&&" ~> AndExpr) ^^ { case cmp ~ and => and match {
                                                                      case None => cmp 
                                                                      case Some(x) => &&(cmp,x)
                                                   }}
      | failure("illegal start of <and> expression")
  )

  
  /** <pre>
   *   CmpExpr ::= ArithExpr [ ( "<" | "<=" | ">" | ">=" | "==" | "!=" ) ArithExpr ]
   *  </pre>
   */
  def CmpExpr: Parser[Expr] = positioned(
        ArithExpr ~ opt( (   "<"   ^^^ createCmpExpr("<") _
                           | "<="  ^^^ createCmpExpr("<=") _
                           | ">"   ^^^ createCmpExpr(">") _
                           | ">="  ^^^ createCmpExpr(">=") _
                           | "=="  ^^^ createCmpExpr("==") _
                           | "!="  ^^^ createCmpExpr("!=") _
                         ) ~ ArithExpr
                       ) ^^ { case lhs ~ opt => opt match {
                                                     case None => lhs 
                                                     case Some(~(op,rhs)) => op(lhs,rhs)
                                    }}
      | failure("illegal start of boolean expression")
  )   
  
  
  /**
   * <p>
   * 	Create a comparison expression. The string 'op' impose which node has to 
   *    be created and allow to desugarize some expression in equaivalent ones.
   * </p>
   * @param op : The comparison string operator
   * @param lhs: The parsed lhs value of the expression
   * @param rhs: The parsed rhs value of the expression
   */
  private def createCmpExpr(op: String)(lhs: Expr,rhs:Expr): Expr = op match {
     case "<" => <(lhs,rhs)
     case "<=" => <=(lhs,rhs)
     case ">" => <(rhs,lhs)
     case ">=" => <=(rhs,lhs)
     case "==" => new ==(lhs,rhs)
     case "!=" => new !(new ==(lhs,rhs))
   }        
  
   
   /**
    * ArithExpr ::= ArithPrecedence { ( "+" | "-" ) ArithExpr }
    */
   def ArithExpr: Parser[Expr] = positioned(
       ArithPrecedence ~rep ( ( "+" ^^^ (ch.epfl.lara.matcheck.ast.+)
                              | "-" ^^^ (ch.epfl.lara.matcheck.ast.-)
                ) ~ ArithExpr) ^^ { case first ~ rest => mkBinaryRelation[Expr](first,rest)}
     | failure("illegal start of arithmetic expression")   
   )
    
   /**
    * ArithPrecedence ::= MatchExpr { ( "%" | "/" | "*" ) ArithPrecedence }
    */
   def ArithPrecedence: Parser[Expr] = positioned(
       MatchExpr ~ rep( (  "%"    ^^^ (ch.epfl.lara.matcheck.ast.%) 
                         | "/"    ^^^ (ch.epfl.lara.matcheck.ast./)
                         | "*"    ^^^ (ch.epfl.lara.matcheck.ast.*) 
                      )  ~ ArithPrecedence )         ^^ { case first ~ rest => mkBinaryRelation[Expr](first,rest)}         
     | failure("illegal start of arithmetic expression")
   )
   
   
  /** <pre>
   *    MatchExpr ::=    ComplexExpr [ "match" "{" { CaseDef } "}" ]
   *		       | ComplexExpr [ "." "isInstanceOf" "[" Type "]"
   *  </pre>
   */
  def MatchExpr: Parser[Expr] = positioned(
      "(" ~> ComplexExpr ~ ":" ~ Type ~ ")" ~ "match" ~ "{" ~ rep(CseDef) <~ "}"  ^^ 
        { case scrut ~ ":" ~ tpe ~ ")" ~ "match" ~ "{" ~ cases  => Match(scrut,tpe,cases.zipWithIndex.map(pair => CaseDef(pair._2, pair._1._1, pair._1._2, pair._1._3)))}
      | ComplexExpr ~ opt( "." ~> "isInstanceOf" ~>"[" ~> Type <~ "]") ^^ { case e ~ tpe => tpe match {
                                                                                             case None => e 
                                                                                             case Some(tpe) => IsInstanceOf(e,tpe)
                                                                              }}
      | failure("illegale start of pattern matching expresison")
  )
  
  
  /** <pre>
   *    CseDef ::= "case" PatDef [ "if" Expr ] => Expr
   *  </pre>
   */
  def CseDef: Parser[(PatternDef,Option[Expr],Expr)] = (
        "case" ~> PatDef ~ opt("if" ~> Expr) ~ "=>" ~ Expr  ^^ { case a ~ b ~ "=>" ~ c => Tuple3(a,b,c)}
      | failure("illegal start of case definition")    
  )
  
  
  /** 
   * PatDef ::=   "_"
   *	        | ident  "(" Patist ")"  
   *		| ident ":" Type
   */
  def PatDef: Parser[PatternDef] = positioned(
        "_" ^^^ Wildcard  
      | ident  ~ "(" ~ PatList ~ ")"  ^^ { case name ~ "(" ~ args ~ ")" => ClassPattern(new Name[ObjectSymbol](name),args)} 
      | ident ~ ":" ~ Type           ^^ { case name ~ ":" ~ tpe  =>   VarPattern(new Name[LocalSymbol](name),tpe) }
      | failure("illegal start of pattern definition")
  )
  
  
  /** <pre>
   *    PatList ::= PatDef { "," PatDef }        
   *  </pre>
   */
  def PatList: Parser[List[PatternDef]] = (
          PatDef ~ rep("," ~> PatDef)  ^^  { case pat ~ pats => pat :: pats}
      | success(Nil: List[PatternDef])
  )
  
    
  /** <pre>
   *    ComplexExpr ::= SimpleExpr { "." ident [ "(" Expressions ")" ] }
   *  </pre>
   */
  def ComplexExpr: Parser[Expr] = positioned(
        SimpleExpr ~  rep("." ~> ident ~ opt("(" ~> Expressions <~ ")")) ^^ { case first ~ rest => mkExpression(first,rest) }
     |  failure("illegal start of expression")                 
  )  
  

  
  def Identifier: Parser[Ident] = positioned(
        ident                        ^^ ({name => Ident(new Name(name))})
      | failure("illegal start of identifier")
  )
  
  
  /** <pre>
   *    SimpleExpr ::=   ident [ "(" Expressions ")" ]
   *		       | "List" "(" Expressions ")"
   *		       | "true"
   *		       | "false"
   *		       | "this"
   *                   | "new" ident "(" Expressions ")"
   *                   | "if" "(" Expr ")" "{" Expr "}" "else" "{" Expr "}"
   *                   | [ "-" ] numericLit
   *                   | stringLit
   *                   | "(" Expr ")"
   *  </pre>
   */
  def SimpleExpr: Parser[Expr] = positioned(
        Identifier ~ opt("(" ~> Expressions <~ ")")            ^^ {case name ~ params => params match {
                                                                                        case None => name 
                                                                                        case Some(p) => Call(ObjectId(new Name(name.name.getName)),new Name[MethodSymbol]("apply"),p)
                                                                   }}
      | "true"                                          ^^^  True
      | "false"                                         ^^^  False
      | "new" ~> ident ~ "(" ~ Expressions ~ ")"         ^^ { case name ~ "(" ~ params ~ ")" => New(new Name(name),params)}
      | "if" ~> "(" ~> Expr ~ ")" ~ "{" ~ Expr ~ "}" ~ 
          "else" ~ "{" ~ Expr <~ "}"                     ^^ {case cond ~ ")" ~ "{" ~ then ~ "}" ~ "else" ~ "{" ~ elze => If(cond,then,elze)}
      | opt("-") ~ numericLit                           ^^ {case neg ~ x => neg match {
                                                                                  case Some("-")  => Number(-x.toInt) 
                                                                                  case _ => Number(x.toInt)
                                                                   }}
      | stringLit                                       ^^ { case x => StringLit(x) } 
      | "(" ~> Expr <~ ")"
      | failure("illegal start of simple expression")
  )

  
  /**
   * <p>
   * 	Dependending on the rest List decide whether to create a Call, Select node or,
   * 	if the list is empty, just return the obj expression.
   * </p>
   */
  private def mkExpression(obj: Expr, rest: List[~[String, Option[List[Expr]]]]) = {
    var t: Expr = obj
    def buildPath(xs: List[~[String, Option[List[Expr]]]]): Unit = xs match {
      case ~(meth, Some(args)) :: rest =>
        t = Call(t, new Name(meth), args)
        buildPath(rest)
      case ~(field, None) :: rest =>
        t = Select(t, new Name(field))
        buildPath(rest)
      case Nil => ()
    }
    buildPath(rest)
    t
  }
 
   
  /**
   * <p>
   *	Depending on the mexpr parameter decide whether to create a match expression
   *	or not.
   * <p>
   */
  def mkMatch(obj: Expr, tpe: String, mexpr: Option[List[CaseDef]]) = mexpr match {
    case Some(cases) => Match(obj,toType(tpe),cases) 
    case None => obj
  }
  
  
  /**
   * <p>
   * 	Map the string type gave in argument to the respective internal representation
   *	for types.
   * </p>
   * @param tpe: The type parsed as a string
   * @return   : The internal type node that correspond to the parsed string type
   */
  def toType(tpe: String): TypeTree = tpe match {
    case "Int" => IntType
    case "Boolean" => BoolType
    case _ => ClassType(tpe)
  }
   
 def toType2(tpe: String, ptpe: Option[TypeTree]): TypeTree = {
   val stpe = toType(tpe)
   ptpe match {
     case None => stpe
     case Some(ptpe) => ParamType(stpe,ptpe)
   }
 }
  
  protected def parse(r: Reader[char]) : ParseResult[Tree] =
    phrase(Prog)(new lexical.Scanner(r))

  protected def parse(string: String) : ParseResult[Tree] =
    parse(StreamReader(new StringReader(string)))
    
  protected def parseFile(fileName: String) : ParseResult[Tree] =
    parse(StreamReader(new InputStreamReader(new FileInputStream(new File(fileName)), "ISO-8859-1")))

}

